i:Id, ds:fpf(Id; x.Type), da:fpf(Knd; k.Type), A:ecl(ds; da), snd:msg-spec(ds; da),
upd:update-spec(ds; da).
update-spec-decl(upd; ds)
 msg-spec-loc-decl(snd; i; da)
 ((fpf-dom(id-deq; mkid{ecl:ut2}; ds)))
 R-Feasible{i:l}
 R-Feasible(ecl-machine{ecl:ut2}(i; ds; da; A; snd; upd))
 (R:es_realizer{i:l}. 
 ((R-has-loc(R; i)))
  R-Feasible{i:l}
  R-Feasible(R)
  l_all(append(ecl-kinds(A); fpf-domain(da));
  l_all(Knd;
  l_all(k.((isrcv(k))
  l_all( (((source(lnk(k)) = i  Id)
  l_all(  subtype_rel(ma-valtype(da; k);
  l_all(  subtype_rel(fpf-cap(R-da(R; destination(lnk(k))); Kind-deq; k; top)))
  l_all(  ((destination(lnk(k)) = i  Id)
  l_all(   subtype_rel(fpf-cap(R-da(R; source(lnk(k))); Kind-deq; k; void);
  l_all(   subtype_rel(fpf-cap(da; Kind-deq; k; void))))))
  R-compat{i:l}
  R-compat(ecl-machine{ecl:ut2}(i; ds; da; A; snd; upd); R)) 

latex

Definitions

x. t(x), guard(T), sq_type(T), if b then t else f fi , prop{i:l}, tt, ff, t  T, P  Q, l_all(L; T; x.P(x)), R-has-loc(R; i), es_realizer{i:l}, mkid{$x:ut2}, b, A, P  Q, update-spec(ds; da), msg-spec(ds; da), ecl(ds; da), fpf(A; a.B(a)), Id, x:A. B(x), x(s), False, P  Q, Unit, ,

Lemmas

msg-item wf, pi2 wf, pi1 wf, nat wf, update-spec-decl wf, msg-spec-loc-decl wf, fpf-trivial-subtype-top, id-deq wf, fpf-dom wf, finite-prob-space wf, decl-type wf, decl-state wf, fpf wf, IdLnk wf, Knd wf, rationals wf, unit wf, R-Feasible wf, top wf, Kind-deq wf, ldst wf, R-da wf, fpf-cap wf, ma-valtype wf, lnk wf, lsrc wf, isrcv wf, fpf-domain wf, append wf, l member wf, ecl-machine-icompat, Id wf, false wf, not functionality wrt iff, assert of bnot, eqff to assert, not wf, bnot wf, R-has-loc wf, true wf, Id sq, assert-eq-id, eqtt to assert, assert wf, iff transitivity, bool wf, eq id wf, msg-spec-loc-decl-implies, ecl-machine-loc, ecl-machine wf, R-compat-disjoint